Module code | COS 741 |
Qualification | Postgraduate |
Faculty | Faculty of Engineering, Built Environment and Information Technology |
Module content | Model Checking is a technique for automatically verifying whether a software program satisfies correctness requirements such as mutual exclusion, deadlock-freedom or starvation-freedom. In contrast to testing, model checking is not only capable of detecting bugs but also of proving their absence. This is of particular importance for safety-critical software used in cars, planes, power plants etc. This module focuses on the theoretical foundations of model checking: modelling the state space of software as an automaton, formal specification of correctness requirements in temporal logic, and algorithms for systematically exploring the state space of software. The practical aspect of this module, includes how to write parallel programs composed of communicating processes. Existing model checking tools will be used to verify the correctness of the programs written. |
Module credits | 15.00 |
NQF Level | 08 |
Programmes | |
Prerequisites | No prerequisites. |
Contact time | 2 lectures per week |
Language of tuition | Module is presented in English |
Department | Computer Science |
Period of presentation | Semester 1 or Semester 2 |
Copyright © University of Pretoria 2024. All rights reserved.
Get Social With Us
Download the UP Mobile App